\section{The Class Cardholder}

This class models a cardholder's name and address. This information is 
used to post an account statement. The class provides standard read/write operations.

\begin{vdm_al}
class Cardholder

types
  public Address = seq of char;
  public Name = seq of char;

instance variables
  name : Name;
  address : Address;

operations
  public Cardholder : Name * Address ==> Cardholder
  Cardholder(nm,addr) ==
    (name := nm;
     address := addr);

  pure public GetName : () ==> Name 
  GetName () ==
    return name;

  pure public GetAddress : () ==> Address 
  GetAddress() ==
    return address;

end Cardholder
\end{vdm_al}